COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST T F ε Proposition
C00007 00003	axiom logic:
C00011 00004	declare INDCONST Tm ε Thingconcept
C00012 ENDMK
C⊗;
declare INDCONST T F ε Proposition;
declare INDVAR Q Q0 Q1 Q2 Q3 Q4 ε Proposition;

DECLARE OPCONST And(Proposition,Proposition) = Proposition [L←655,R←650];
DECLARE OPCONST Or(Proposition,Proposition) = Proposition [L←635,R←640];
DECLARE OPCONST Implies(Proposition,Proposition) = Proposition [L←615,R←620];
DECLARE OPCONST Equiv(Proposition,Proposition) = Proposition [L←605,R←610];
DECLARE OPCONST Not(Proposition) = Proposition [R←675];
DECLARE OPCONST All(Thingvariable,Proposition) = Proposition;

DECLARE OPCONST Concept1(thing) → Thingconcept [R ← 800];

DECLARE OPCONST Subst(Thingconcept,Thingvariable,Thingconcept) = Thingconcept;
DECLARE OPCONST Substp(Thingconcept,Thingvariable,Proposition) = Proposition;

declare INDVAR X X0 X1 X2 X3 X4 ε Thingconcept;
declare INDVAR x x0 x1 x2 x3 x4 ε thing;
declare OPCONST Equal(Thingconcept,Thingconcept) = Proposition [L←685,R←690];

declare INDVAR V V0 V1 V2 V3 V4 ε Thingvariable;
declare INDCONST VV VV0 VV1 VV2 VV3 VV4 ε Thingvariable;


declare INDCONST world ε worlds;
declare INDVAR w w1 w2 w3 w4 ε worlds;

declare PREDCONST ttrue(Proposition) [R←600];
declare PREDCONST true(worlds,Proposition);
declare OPCONST Nec(Proposition) = Proposition [R←700];
declare PREDCONST nec(Proposition) [R←600];
declare PREDCONST prec(worlds,worlds) [inf];

declare OPCONST denot(worlds,Thingconcept) = thing;

declare INDCONST Mike Joe Pat ε Personconcept;
declare INDCONST mike joe pat ε person;
declare INDVAR P P1 P2 P3 P4 ε Personconcept;
declare INDVAR p p1 p2 p3 p4 ε person;
declare INDVAR PV PV1 PV2 PV3 PV4 ε Personvariable;
declare INDCONST PPV PPV1 PPV2 PPV3 PPV4 ε Personvariable;

moregeneral Thingconcept ≥ {Personconcept,Thingvariable};
moregeneral thing ≥ {person};
moregeneral Personconcept ≥ {Personvariable};
moregeneral Thingvariable ≥ {Personvariable};

declare OPCONST Telephone(Personconcept) = Thingconcept[R←710];
declare OPCONST telephone(person) = thing [R←599];
axiom teldef:	∀P w.(denot(w,Telephone P) = telephone denot(w,P));;

declare OPCONST K(Personconcept,Proposition) = Proposition;
declare PREDCONST k(person,Proposition);

declare OPCONST Know(Personconcept,Thingconcept) = Proposition;
declare PREDCONST know(person,Thingconcept);

declare OPCONST Want(Personconcept,Proposition) = Proposition;
declare PREDCONST want(person,Proposition);

declare OPCONST Like(Personconcept,Personconcept) = Proposition;
declare PREDCONST like(person,Personconcept);

declare OPCONST Future(Proposition) = Proposition [R←695];
declare PREDCONST future(Proposition) [R←597];

declare INDVAR E E0 E1 E2 E3 E4 ε Eventconcept;
declare INDVAR A A0 A1 A2 A3 A4 ε Actionconcept;

declare OPCONST Cause(Eventconcept,Proposition) = Proposition;
declare OPCONST Do(Personconcept,Actionconcept) = Eventconcept;
declare OPCONST Occur(Eventconcept) = Proposition [R←695];
declare OPCONST Tell(Personconcept,Thingconcept) = Actionconcept;
axiom logic:
	∀Q1 Q2 w.(true(w,Q1 And Q2) ≡ true(w,Q1) ∧ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Or Q2) ≡ true(w,Q1) ∨ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Implies Q2) ≡ true(w,Q1) ⊃ true(w,Q2))
	∀Q1 Q2 w.(true(w,Q1 Equiv Q2) ≡ (true(w,Q1) ≡ true(w,Q2)))
	∀Q w.(true(w,Not Q) ≡ ¬true(w,Q))

	∀V Q w.(true(w,All(V,Q)) ≡ ∀x.(true(w,Subst(Concept1 x,V,Q))))
;;

axiom concept:
	∀x w.(denot(w,Concept1 x) = x)
;;

axiom subst:
	∀X V V.(Subst(X,V,V) = X)
	∀X V1 V2.(¬V1=V2 ⊃ Subst(X,V1,V2) = V2)
;;

axiom future:
	∀Q w.(true(w,Q) ⊃ true(w,Future Q))
	∀Q w.(true(w,Future Future Q) ⊃ true(w,Future Q))
	∀w Q.(true(w,Future Q) ≡ ∃w1.(w prec w1 ∧ true(w1,Q)))
;;

axiom tell:
	∀P1 P2 X w.(true(w,Know(P1,X)) 
⊃ true(w,Cause(Do(P1,Tell(P2,X)),Know(P2,X))))
	∀P1 P2 Q w.(true(w,K(P1,Q)) ⊃ true(w,Cause(Do(P1,Tell(P2,Q)),K(P2,Q))))
;;

axiom likewant:
	∀P1 P2 Q w.(true(w,Like(P1,P2)) ∧ true(w,K(P1,Want(P2,Q)))
⊃ true(w,Want(P1,Q)))
;;

axiom cause:
	∀E Q1 Q2 w.(true(w,Cause(E,Q1)) ∧ true(w,Cause(E,Q2))
⊃ true(w,Cause(E,Q1 And Q2)))
	∀E Q w.(true(w,Occur E) ∧ true(w,Cause(E,Q)) ⊃ true(w,Future Q))
;;

axiom wantdo:
	∀P Q A w.(true(w,Want(P,Q)) ∧ true(w,K(P,Occur Do(P,A) Implies Future Q))
⊃ true(w,Occur Do(P,A)))
;;

axiom nec:
	∀P Q.(∀w.true(w,Q) ⊃ ∀w.true(w,K(P,Q)))
;;

axiom introspection:
	∀P X w.(true(w,Know(P,X)) ⊃ true(w,K(P,Know(P,X))))
	∀P Q w.(true(w,K(P,Q)) ⊃ true(w,K(P,K(P,Q))))
	∀P X w.(true(w,Want(P,X)) ⊃ true(w,K(P,Want(P,X))))
	∀P1 P2 w.(true(w,Like(P1,P2)) ⊃ true(w,K(P1,Like(P1,P2))))
	∀P Q1 Q2 w.(true(w,K(P,Q1)) ∧ true(w,K(P,Q1 Implies Q2)) ⊃ true(w,K(P,Q2)))
;;

axiom knoweq:
∀P X1 X2 w.(true(w,Know(P,X1)) ∧ true(w,(Know(P,X2))
∧ true(w,Equal(X1,X2)) ⊃ true(w,K(P,Equal(X1,X2))))
;;
declare INDCONST Tm ε Thingconcept;
axiom problem1:
	true(world,Know(Pat,Tm))
	true(world,Want(Pat,Know(Joe,Tm)))
;;

axiom problem2:
	true(world,Want(Joe,Know(Joe,Tm)))
	true(world,K(Joe,Know(Pat,Tm)))
	true(world,K(Joe,Like(Pat,Joe)))
;;